$Q$ $\leftarrow$==$f$== $P$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$e$:\{$e$:E$\mid$ $P$($e$)\} . $f$($e$) c$\leq$ $e$ \& $Q$($f$($e$))